\begin{tabbing}
$M$.rframe($A$.pre $p$ for $a$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=IdIdDeq$\forall$$x$$\in$dom(($M$.2.2.2.2.2.2.2.2.2.2).1). \+
\\[0ex]
\\[0ex]$L$\==($M$.2.2.2.2.2.2.2.2.2.2).1($x$) $\Rightarrow$ \+
\\[0ex]($\uparrow$deq{-}member(KindDeq;locl($a$);$L$))
\-\\[0ex]$\vee$ ($\forall$$s_{1}$:$A$.state, $s_{2}$:$A$.state. ma{-}x{-}equiv($A$;$x$;$s_{1}$;$s_{2}$) $\Rightarrow$ ($p$($s_{1}$) = $p$($s_{2}$) $\in$ $\mathbb{B}$))
\-
\end{tabbing}